T:Type, L:T List, R:({x:T| (x  L) }Realizer), A:Realizer.
xL.R(x) || A  (x:T. (x  L)  R(x) || A) 

latex

Definitions	x:A. B(x), P  Q, x(s), P  Q, t  T, P & Q, P  Q, x. t(x), Prop
Lemmas	R-compat-Rall, R-compat-symmetry, Rall wf, l member wf, R-compat wf, es realizer wf